module Data

sig Data {
	ora : one Int,
	giorno : one Int,
	mese : one Int,
	anno : one Int
}
{
	ora >= 0 and ora < 24
	giorno >= 1 and giorno <= 31
	mese >= 1 and mese <= 12
	(mese = 4 or mese = 6 or mese = 9 or mese = 1) => giorno <=30
	mese = 2 implies giorno <= 28
}

pred uguale[d1, d2: Data]  {
	d1.anno = d2.anno and d1.mese = d2.mese and d1.giorno = d2.giorno and d1.ora = d2.ora
}

pred precede[d1, d2: Data] {
	(d1.anno < d2.anno) or
	(d1.anno = d2.anno and d1.mese < d2.mese) or
	(d1.anno = d2.anno and d1.mese = d2.mese and d1.giorno < d2.giorno) or
	(d1.anno = d2.anno and d1.mese = d2.mese and d1.giorno = d2.giorno and d1.ora < d2.ora)
}

pred precedeOrEqual[d1, d2: Data] {
	precede[d1,d2] or uguale[d1,d2]
}

pred succede[d1, d2: Data] {
	//nota: gli argomenti sono invertiti
	precede[d2,d1]
}

pred succedeOrEqual[d1,d2:Data] {
	// se una data non precede l'altra, allora sono per forza o uguali o successive
	not precede[d1,d2]
}
